Trait isotope::ctx::eval::ReductionConfig[][src]

pub trait ReductionConfig {
    type AsRef: ReductionConfig;
    fn register_push_subst(&mut self, subst: &TermId) -> Result<(), Error>;
fn register_pop_subst(&mut self) -> Result<(), Error>;
fn register_beta(&mut self) -> Result<(), Error>;
fn register_eta(&mut self) -> Result<(), Error>;
fn eta(
        &self,
        term: &Term,
        ctx: &mut impl TyCtxMut + ?Sized
    ) -> Result<bool, Error>;
fn sub(
        &self,
        term: &Term,
        ctx: &mut impl TyCtxMut + ?Sized
    ) -> Result<bool, Error>;
fn head(
        &self,
        term: &Term,
        ctx: &mut impl TyCtxMut + ?Sized
    ) -> Result<bool, Error>;
fn intersects(&self, filter: VarFilter, code: Code, form: Form) -> bool;
fn as_ref_mut(&mut self) -> &mut Self::AsRef; }
Expand description

A reduction configuration

Associated Types

Get this reduction configuration as a reference

Required methods

Register a pushed substitution.

Register a popped substitution.

Register a beta reduction: return whether to terminate beta reduction (Error::StopReduction)

Register an eta reduction: return whether to terminate eta reduction (Error::StopReduction)

Given a term, whether to attempt an eta reduction or terminate (Error::StopReduction)

Given a term, whether to attempt a subterm reduction or terminate (Error::StopReduction)

Given a term, whether to attempt a head reduction or terminate (Error::StopReduction)

Get whether a term with the given filter intersects with this context

Get this reduction configuration as a mutable reference

Implementations on Foreign Types

Implementors